#include <clock/clock.h>
#include <cspace/cspace.h>
#include <fcntl.h>
#include <sos.h>
#include <stdlib.h>
#include <string.h>
#include <nfs/nfs.h>
#include <nfs/time.h>
#include <libut.h>

#include "list.h"
#include "macros.h"
#include "nfs.h"
#include "pagetable.h"
#include "picoro.h"
#include "task.h"
#include "vfs.h"
#include "vmem_layout.h"

#include "debug.h"
#define verbose SOS_DEBUG_NFS
#include <sys/debug.h>
#include <sys/panic.h>

/* Frequency of nfs_timeout() in microseconds */
#define SOS_NFS_TICK     (100000)
/* Size of the key used in the NFS FD table (for libut) */
#define SOS_NFS_KEYSIZE  (FHSIZE)
/* The most we request from NFS in a single read (4KiB) */
#define SOS_NFS_MAX_READ  (4096)
#define SOS_NFS_MAX_WRITE (4096)
/* The number of seconds between the 1900 (TIME) and 1970 (Unix) epochs */
#define EPOCHDIFF        (2208988800L)

/* Bitmasks for Unix octal permissions */
#define USER_READ         (0b100000000)
#define USER_WRITE        (0b010000000)
#define USER_EXEC         (0b001000000)
#define GROUP_READ        (0b000100000)
#define GROUP_WRITE       (0b000010000)
#define GROUP_EXEC        (0b000001000)
#define OTHERS_READ       (0b000000100)
#define OTHERS_WRITE      (0b000000010)
#define OTHERS_EXEC       (0b000000001)
#define ANY_READ          (USER_READ | GROUP_READ | OTHERS_READ)
#define ANY_WRITE         (USER_WRITE | GROUP_WRITE | OTHERS_WRITE)
#define ANY_EXEC          (USER_EXEC | GROUP_EXEC | OTHERS_EXEC)
/* Macros for our very simplified interpretation of Unix permissions */
#define MODE_CAN_READ(x)  ((x) & (ANY_READ))
#define MODE_CAN_WRITE(x) ((x) & (ANY_WRITE))
#define MODE_CAN_EXEC(x)  ((x) & (ANY_EXEC))

/* An individual entry in the FD table.                                       */
/* fs_fds are just pointers to this struct                                    */
/* We assume that any given PID will have at most one task waiting for resume */
/* Each callback will have a pointer to this FDE, allowing resume + cleanup.  */
/* If SOS supported threaded applications, this assumption breaks, hard.      */
typedef struct nfs_fd_entry {
    fhandle_t fh;      /* NFS filehandle provided by libnfs */
    fmode_t mode;      /* Store access permissions in the SOS format */
    coro task;         /* Pending task for the given handle */
    size_t seek;       /* Seekpoint */
    int abort;         /* If an operation is in progress, tell it to abort */

    /* libut manages the FD table as a doubly-linked list */
    struct nfs_fd_entry *next;
    struct nfs_fd_entry *prev;
} nfs_fd_entry;

/* libut manipulates this pointer as a hash table. */
static struct nfs_fd_entry *_fd_table;

/* Currently, NFS mounting is taken care of by network.c */
extern fhandle_t mnt_point;

/* We use the TIME server to get and store our startup time */
static seL4_Word _time_boot_unix;

/* SOS VFS expects these functions - main interface to this module */
static int _mount(sos_mount *mount, const char *fs_data);
static int _umount(sos_mount *mount, const char *fs_data);

static int _open(sos_pcb *pcb, const char* path, fmode_t mode,
                 int proc_fd, seL4_Word *fs_fd);
static int _close(sos_pcb *pcb, seL4_Word fs_fd);
static int _read(sos_pcb *pcb, seL4_Word fs_fd, char* buf, size_t nbyte);
static int _write(sos_pcb *pcb, seL4_Word fs_fd, char* buf, size_t nbyte);
static int _getdirent(sos_pcb *pcb, int pos, size_t max);
static int _stat(sos_pcb *pcb, const char *path);

/* Forward declarations for various internal utility functions */
static inline void _register_timeout();
static void _timeout_callback(uint32_t id, void *data);

/* Convert nfs stat enum codes to valid VFS errors */
static inline int _nfs_stat_translate(enum nfs_stat stat) {
    switch (stat) {
        case NFS_OK :
            return SOS_VFS_SUCCESS;
            break;

        case NFSERR_PERM :
            return SOS_VFS_PERM;
            break;

        case NFSERR_NOENT :
            return SOS_VFS_NOENT;
            break;

        default:
            return SOS_VFS_INVAL;
    }
}

/* Convert rpc stat enum codes to valid VFS errors */
static inline int _rpc_stat_translate(enum rpc_stat stat) {
    switch(stat) {
        case RPC_OK :
            return SOS_VFS_SUCCESS;
            break;
        case RPCERR_NOMEM :
            return SOS_VFS_OOM;
            break;
        case RPCERR_NOBUF :
            return SOS_VFS_OOM;
            break;
        default:
            return SOS_VFS_INVAL;
    }
}

/* Convert timeval_t to sos_stat_t time */
static inline long _timeval_sos(timeval_t time) {
    if (time.seconds > _time_boot_unix) {
        return (long) (1000 * (time.seconds - _time_boot_unix));
    } else {
        return 0;
    }
}

/* Create the structure for a single FD entry, and provide its fs_fd       */
/* (this does not insert it into the FD table - we don't have a fhandle_t) */
static inline int _nfs_create_fd(seL4_Word *fd) {
    nfs_fd_entry *fde = malloc(sizeof(struct nfs_fd_entry));
    if (fde == NULL) return SOS_VFS_OOM;
    // Clear out the allocated memory
    memset(fde, 0x00, sizeof(struct nfs_fd_entry));
    (*fd) = (seL4_Word) fde;
    return SOS_VFS_SUCCESS;
}

/* Look up an nfs_fd_entry, given an fs_fd. */
/* Right now these are the same, so this is a cast; may not always be the case */
static inline int _nfs_lookup_fd(seL4_Word fs_fd, nfs_fd_entry **fd) {
    // Literally cast the pointer
    (*fd) = (nfs_fd_entry *) fs_fd;
    return SOS_VFS_SUCCESS;
}

/* Insert a given fs_fd into the fd table with the key fh */
static inline int _nfs_insert_fd(seL4_Word fs_fd, fhandle_t *fh) {
    nfs_fd_entry *fde;
    _nfs_lookup_fd(fs_fd, &fde);
    // Add to the FD table
    DL_APPEND(_fd_table, fde);
    return SOS_VFS_SUCCESS;
}

/* Delete a fs_fd from the fd table, and free its memory */
static inline int _nfs_delete_fd(seL4_Word fs_fd) {
    // lookup fd
    nfs_fd_entry *fd;
    _nfs_lookup_fd(fs_fd, &fd);
    // Remove from the FD table
    DL_DELETE(_fd_table, fd);
    // Free the memory
    free(fd);
    return SOS_VFS_SUCCESS;
}

/* Callback function for our 100ms timer tick */
static void _timeout_callback(uint32_t id, void *data) {
    // dprintf(9, "nfs_timeout_callback: firing\n");
    nfs_timeout();
    _register_timeout();
}

/* Register the next NFS tick */
static inline void _register_timeout(void) {
    register_timer(SOS_NFS_TICK, &_timeout_callback, NULL);
}

/* Provide the sos_filesystem object that we pass into various VFS */
int sos_nfs_init(sos_filesystem **fs) {
    int err;
    struct ip_addr gw;

    // Register the NFS timeout.
    _register_timeout();

    // Allocate some memory for the fs object
    dprintf(1, "\tCreating NFS filesystem object...\n");
    (*fs) = malloc(sizeof(struct sos_filesystem));
    if ((*fs) == NULL) return SOS_NFS_OOM;

    // Populate it with our function pointers
    (**fs) = (sos_filesystem) { _mount, _umount };

    // Store an initial timestamp
    err = ipaddr_aton(CONFIG_SOS_GATEWAY, &gw);
    if (!err) return SOS_NFS_INVAL;
    _time_boot_unix = udp_time_get(&gw);
    // TIME sends seconds since 1900 - we need to convert it to epoch
    _time_boot_unix -= EPOCHDIFF;

    return SOS_NFS_SUCCESS;
}

/* Destroy the sos_filesystem object */
// XXX Implement this one day
int sos_nfs_destroy(sos_filesystem *fs) {
    return SOS_NFS_INVAL;
}

static int _mount(sos_mount *mount, const char *fs_data) {
    if (mount == NULL) return SOS_VFS_INVAL;
    (*mount) = (sos_mount) {
        .open = &_open,
        .close = &_close,
        .read = &_read,
        .write = &_write,
        .getdirent = &_getdirent,
        .stat = &_stat
    };
    return SOS_VFS_SUCCESS;
}

static int _umount(sos_mount *mount, const char *fs_data) {
    return SOS_VFS_INVAL;
}

/* Callback given to nfs_lookup. Token is a pointer to FDE. */
void _lookup_cb(uintptr_t token, enum nfs_stat status,
                   fhandle_t *fh, fattr_t *fattr) {
    int err;
    nfs_fd_entry *fd = (nfs_fd_entry *) token;

    // Let the coroutine know the operation status.
    resume(fd->task, (void *) status);
    resume(fd->task, (void *) fattr);
    resume(fd->task, (void *) fh);
    return;
}

static void _create_cb(uintptr_t token, enum nfs_stat status,
                       fhandle_t *fh, fattr_t *fattr) {
    nfs_fd_entry *fd = (nfs_fd_entry *) token;
    resume(fd->task, (void *) status);
    resume(fd->task, (void *) fh);
    return;
}

static void *_open_task(void *arg) {
    int err;
    fattr_t *fattrs;
    list args = (list) arg;

    assert(args->size == 5);

    dprintf(6, "nfs_open_task: Removing arguments from list\n");
    int proc_fd = (int) list_pop_front(args);
    sos_pcb *pcb = (sos_pcb *) list_pop_front(args);
    fmode_t mode = list_pop_front(args);
    nfs_fd_entry *fd = (nfs_fd_entry *) list_pop_front(args);
    char *_path = (char *) list_pop_front(args);
    char path[SOS_PATH_MAX] = { 0 };

    // Copy that string across before the caller wipes the memory
    strncpy(path, _path, SOS_PATH_MAX);

    // Let caller continue; we'll be woken up by network irq to call back
    // Grab the callback status from nfs_lookup, see if we can continue
    dprintf(6, "nfs_open_task: Yielding for lookup callback\n");
    err = (int) yield(NULL);
    fattrs = (fattr_t *) yield(NULL);
    fhandle_t *fh = (fhandle_t *) yield(NULL);

    // Check for abort - it is possible after each yield
    if (fd->abort) {
        dprintf(6, "nfs_open_task: operation aborted\n");
        _nfs_delete_fd((seL4_Word) fd);
        free(pcb);
        return NULL;
    }

    dprintf(6, "nfs_open_task: Completing operation\n");
    if (err == NFSERR_NOENT) {
        // We need to set up a 'create' call
        sattr_t sattr = {
             // XXX If we enforce the 'fmode_t mode', we break cp in sosh!
            .mode = ANY_WRITE | ANY_READ,
            .uid = 1,
            .gid = 1,
            .size = 0,
            .atime = 0,
            .mtime = 0
        };
        timestamp_t ts = time_stamp();
        sattr.atime.seconds = _time_boot_unix + (ts / 1000000);
        sattr.mtime.seconds = _time_boot_unix + (ts / 1000000);
        nfs_create(&mnt_point, path, &sattr, &_create_cb,
                   (uintptr_t) fd);
        err = (int) yield(NULL);
        fh = (fhandle_t *) yield(NULL);
    }

    // Abort possible during nfs_create call
    if (fd->abort) {
        dprintf(6, "nfs_open_task: operation aborted\n");
        _nfs_delete_fd((seL4_Word) fd);
        free(pcb);
        return NULL;
    }

    if (err) {
        dprintf(3, "nfs_open_task: bad nfs_stat (%d)\n", err);
        // Cleanup (via syscall -> vfs) and wake up thread
        sos_syscall_open_reply(pcb, proc_fd, _nfs_stat_translate(err));
        fd->task = NULL;
        return NULL;
    }

    /* Store SOS filemode in the FD */
    fd->mode = mode;

    /* Copy the filehandle */
    memcpy(&(fd->fh), fh, SOS_NFS_KEYSIZE);

    // Enforce filemode against attrs here. fattrs must match mode
    err = SOS_VFS_SUCCESS;
    if (!MODE_CAN_READ(fattrs->mode) && (mode == O_RDONLY || mode == O_RDWR)) {
        dprintf(3, "nfs_open_task: NFS attributes prohibit reads\n");
        dprintf(3, "nfs_open_task: attributes %x\n", fattrs->mode);
        err = SOS_VFS_PERM;
    }

    if (!MODE_CAN_WRITE(fattrs->mode) && (mode == O_WRONLY || mode == O_RDWR)) {
        dprintf(3, "nfs_open_task: NFS attributes prohibit writes\n");
        err = SOS_VFS_PERM;
    }

    /* Clear the coro pointer - we don't want this coro to be resumed ever again */
    fd->task = NULL;

    /* Call back process. If errors occurred, a close op will follow. */
    sos_syscall_open_reply(pcb, proc_fd, err);

    dprintf(3, "nfs_open_task is finished\n");
    return NULL;
}

static int _open(sos_pcb *pcb, const char* path, fmode_t mode,
                 int proc_fd, seL4_Word *fs_fd) {
    int err;
    nfs_fd_entry *fd;
    enum rpc_stat stat;

    dprintf(5, "nfs_open: %.128s...\n", path);

    dprintf(7, "nfs_open: fs_fd was %p\n", *fs_fd);

    /* Allocate a FDE */
    err = _nfs_create_fd(fs_fd);
    if (err) return err;

    dprintf(7, "nfs_open: fs_fd is now %p\n", *fs_fd);

    // Translate the given fs_fd to a fde pointer
    err = _nfs_lookup_fd(*fs_fd, &fd);
    if (err) return err;

    /* Insert FD into table */
    _nfs_insert_fd((seL4_Word) fd, NULL);

    // Add mode and FD address to the coroutine arguments
    list args = list_init();
    err  = list_push_back(args, (SOS_LIST_TYPE) proc_fd);
    err |= list_push_back(args, (SOS_LIST_TYPE) pcb);
    err |= list_push_back(args, (SOS_LIST_TYPE) mode);
    err |= list_push_back(args, (SOS_LIST_TYPE) fd);
    err |= list_push_back(args, (SOS_LIST_TYPE) path);
    if (err) {
        sos_syscall_open_reply(pcb, proc_fd, err);
        list_destroy(args);
        return err;
    }

    // Create coroutine and supply it with initial arguments; stash away in FD
    fd->task = coroutine(&_open_task);
    dprintf(3, "First run of coroutine at %p\n", fd->task);
    resume(fd->task, (void *) args);

    // Destroy list - should be copied
    list_destroy(args);

    // Set up async NFS operation
    stat = nfs_lookup(&mnt_point, path, &_lookup_cb, (uintptr_t) (*fs_fd));

    err = _nfs_stat_translate(stat);
    if (err) _nfs_delete_fd(*fs_fd);

    // Return to caller
    return err;
}

static int _close(sos_pcb *pcb, seL4_Word fs_fd) {
    // Delete item from the fd table, if it was in there
    // (We have to assume we're getting a valid fs_fd - VFS can't lose info)
    nfs_fd_entry *fd = (nfs_fd_entry *) fs_fd;
    if (fd->task != NULL && resumable(fd->task)) {
        // An operation is in progress
        fd->abort = 1;
    } else {
        // We are free to delete the FD
        _nfs_delete_fd(fs_fd);
    }
    return SOS_VFS_SUCCESS;
}

void _read_cb(uintptr_t token, enum nfs_stat status, fattr_t *fattr,
              int count, void *data) {
    int err;
    // Use token to figure out who we're meant to be talking to
    nfs_fd_entry *fd = (nfs_fd_entry *) token;

    // resume its coroutine with the error code
    resume(fd->task, (void *) status);
    if (resumable(fd->task)) {
        // resume again with the count
        resume(fd->task, (void *) count);
        // resume again with the data
        resume(fd->task, (void *) data);
    }

    // return, implicitly freeing the data buffer (read better be finished!)
    return;
}

static void _read_pin_cb(int err, seL4_Word sos_vaddr, void *cookie) {
    nfs_fd_entry *fd = (nfs_fd_entry *) cookie;
    resume(fd->task, (void *) err);
    resume(fd->task, (void *) sos_vaddr);
    return;
}

static void *_read_task(void *arg) {
    // Grab our arguments from the list on the stack
    list args = (list) arg;

    assert(args->size == 4);
    sos_pcb *pcb = (sos_pcb *) list_pop_front(args);
    char *buf = (char *) list_pop_front(args);
    size_t nbyte = (size_t) list_pop_front(args);
    nfs_fd_entry *fde = (nfs_fd_entry *) list_pop_front(args);

    int err = SOS_VFS_SUCCESS;
    size_t sent = 0;
    seL4_Word cur_vaddr = (seL4_Word) buf;
    seL4_Word sos_vaddr;
    size_t max_send;
    int recv;
    int nsent;

    seL4_MessageInfo_t reply;

    dprintf(3, "nfs_read_task: Reader task running. Want %dB\n", nbyte);

    while (sent < nbyte) {
        // We want to be able to complete the read with a single copyin
        // .. this means we only read up to nearest page boundary at a time.
        max_send = MIN(nbyte, PAGE_REMAINING(cur_vaddr));

        // pin page so it can't be swapped out under us
        err = sos_page_pin(pcb, cur_vaddr, &_read_pin_cb, (void *) fde);
        err = (int) yield(NULL);
        sos_vaddr = (seL4_Word) yield(NULL);

        // Check for abort
        if (fde->abort && !err) {
            // Page is pinned. hand the frame back to FT
            frame_free(sos_vaddr);
        }
        if (fde->abort) {
            dprintf(6, "nfs_read: aborting operation\n");
            // Delete the FD and free the pcb
            _nfs_delete_fd((seL4_Word) fde);
            free(pcb);
            return NULL;
        }

        if (err) {
            // Check for segfault
            if (err == SOS_PAGE_TABLE_SEGFAULT) {
                dprintf(1, "PID %d segfault, access violation\n", pcb->pid);
                cspace_free_slot(cur_cspace, pcb->reply_cap);
                process_delete(pcb, NULL, NULL);
                return NULL;
            } else break;
            // Just end the read in other circumstances
        }

        // Set up NFS call
        dprintf(7, "nfs_read_task: reading %dB\n", max_send);
        err = nfs_read(&(fde->fh), fde->seek, max_send,
                       &_read_cb, (uintptr_t) fde);

        if (err) {
            dprintf(6, "nfs_read_task: got nfs error (%d)\n", err);
            err = _rpc_stat_translate(err);
            sos_page_release(pcb, cur_vaddr);
            break;
        }

        // XXX Too many context switches here! Use a struct
        // Yield and later receive error code from NFS callback
        dprintf(6, "nfs_read_task: going to sleep\n");
        err = (int) yield(NULL);

        // Check for abort
        if ((fde->abort || pcb->abort) && !err) {
            dprintf(6, "nfs_read: aborting operation\n");
            // Free the pinned frame - it's our responsibility
            frame_free(sos_vaddr);
        }
        if (fde->abort || pcb->abort) {
            _nfs_delete_fd((seL4_Word) fde);
            free(pcb);
            return NULL;
        }

        err = _nfs_stat_translate(err);
        dprintf(5, "nfs_read_task: woken up by NFS callback (err %d)\n", err);
        if (err) {
            sos_page_release(pcb, cur_vaddr);
            break;
        }

        // Yield and immediately receive the number of bytes to read
        recv = (int) yield(NULL);
        dprintf(5, "nfs_read_task: allowed to read %dB\n", recv);

        // Yield and immediately receive the address of data to copy
        buf = (char *) yield(NULL);
        dprintf(5, "nfs_read_task: reading %d from %p\n", recv, buf);

        // Assume libNFS gives up altogether, or the file is shorter than desired
        if (recv == 0) {
           sos_page_release(pcb, cur_vaddr);
           break;
        }

        // Perform a copyin (this checks permissions for us)
        dprintf(5, "received %d bytes\n", recv);
        err = sos_copyin_nofault(pcb, cur_vaddr, buf, recv, &recv);
        dprintf(5, "copied %d bytes\n", recv);

        // Release the page
        sos_page_release(pcb, cur_vaddr);

        if (err) break;

        fde->seek += recv;
        sent += recv;
        cur_vaddr += recv;
    }

    // Wake up the calling process
    dprintf(6, "nfs_read_task: Read %d bytes. Calling back...\n", sent);
    sos_syscall_read_reply(pcb, err, sent);
    return NULL;
}


static int _read(sos_pcb *pcb, seL4_Word fs_fd, char* buf, size_t nbyte) {

    int err;
    list args;
    nfs_fd_entry *fde;

    if (nbyte == 0) {
        sos_syscall_read_reply(pcb, SOS_VFS_SUCCESS, 0);
        return SOS_VFS_SUCCESS;
    }

    if (buf == NULL) {
        sos_syscall_read_reply(pcb, SOS_VFS_INVAL, 0);
        return SOS_VFS_INVAL;
    }

    // Grab FDE pointer
    err = _nfs_lookup_fd(fs_fd, &fde);
    if (err) {
        sos_syscall_read_reply(pcb, err, 0);
        return err;
    }

    // Check we are allowed to read from this FD
    if (fde->mode != O_RDONLY && fde->mode != O_RDWR) {
        dprintf(6, "nfs_read: mode is (%d), can't read\n", fde->mode);
        sos_syscall_read_reply(pcb, SOS_VFS_PERM, 0);
        return SOS_VFS_PERM;
    }

    // Pass arguments to the coroutine via a list
    args = list_init();
    err  = list_push_back(args, (SOS_LIST_TYPE) pcb);
    err |= list_push_back(args, (SOS_LIST_TYPE) buf);
    err |= list_push_back(args, (SOS_LIST_TYPE) nbyte);
    err |= list_push_back(args, (SOS_LIST_TYPE) fde);
    if (err) {
        // Kernel is probably out of memory.
        dprintf(3, "nfs_read: Could not allocate task args (%d)\n", err);
        list_destroy(args);
        sos_syscall_read_reply(pcb, err, 0);
        return SOS_VFS_OOM;
    }

    // Create the coroutine that will do all the actual reading
    fde->task = coroutine(&_read_task);
    // Send its initial arguments
    resume(fde->task, (void *) args);
    list_destroy(args);

    return SOS_VFS_SUCCESS;
}

void _write_cb(uintptr_t token, enum nfs_stat status, fattr_t *fattr, int count) {
    int err;
    // Use token to figure out who we're meant to be talking to
    nfs_fd_entry *fd = (nfs_fd_entry *) token;

    // resume its coroutine with the error code
    resume(fd->task, (void *) status);
    if (resumable(fd->task)) {
        // resume again with the count
        resume(fd->task, (void *) count);
    }
    return;
}

void _write_pin_cb(int err, seL4_Word sos_vaddr, void *cookie) {
    nfs_fd_entry *fd = (nfs_fd_entry *) cookie;
    resume(fd->task, (void *) err);
    resume(fd->task, (void *) sos_vaddr);
    return;
}

static void* _write_task(void *arg) {
    // Grab our arguments from the list on the stack
    list args = (list) arg;

    assert(args->size == 4);
    sos_pcb *pcb = (sos_pcb *) list_pop_front(args);
    char *buf = (char *) list_pop_front(args);
    size_t nbyte = (size_t) list_pop_front(args);
    nfs_fd_entry *fde = (nfs_fd_entry *) list_pop_front(args);

    int err = SOS_VFS_SUCCESS;
    size_t sent = 0;
    seL4_Word cur_vaddr = (seL4_Word) buf;
    seL4_Word sos_kaddr;
    seL4_Word sos_vaddr;
    size_t max_send;
    int recv;
    page_attrs attrs;

    seL4_MessageInfo_t reply;

    while (sent < nbyte) {
        // Pin page
        err = sos_page_pin(pcb, cur_vaddr, &_write_pin_cb, (void *) fde);
        err = (int) yield(NULL);
        sos_kaddr = (seL4_Word) yield(NULL);

        // Check for abort
        if (fde->abort && !err) {
            // Page has been pinned, hand it back to FT
            frame_free(sos_kaddr);
        }
        if (fde->abort) {
            dprintf(6, "nfs_write: aborting operation\n");
            // Delete the FD and clear up the cap - PCB no longer exists
            _nfs_delete_fd((seL4_Word) fde);
            free(pcb);
            return NULL;
        }

        if (err) {
            // Kill process on segfault
            if (err == SOS_PAGE_TABLE_SEGFAULT) {
                dprintf(1, "PID %d segfault, access violation\n", pcb->pid);
                cspace_free_slot(cur_cspace, pcb->reply_cap);
                process_delete(pcb, NULL, NULL);
                return NULL;
            } else break;
        }

        // Look up kernel address and attributes
        err = sos_page_lookup_nofault(pcb, cur_vaddr, &sos_vaddr, &attrs);
        if (err) break;

        // Avoid alignment problems
        sos_vaddr = PAGE_ALIGN(sos_vaddr) + (cur_vaddr & PAGE_MASK);

        // Check permissions
        if (!attrs.readable) {
            err = SOS_VFS_SEGFAULT;
            break;
        }

        // Compute max send
        max_send = MIN(PAGE_REMAINING(sos_vaddr), (nbyte - sent));

        // Set up NFS call
        dprintf(7, "nfs_write_task: %dB from %p\n", max_send, sos_vaddr);
        err = nfs_write(&(fde->fh), fde->seek, max_send, sos_vaddr,
                        &_write_cb, (uintptr_t) fde);
        err = _rpc_stat_translate(err);
        if (err) break;

        err = (int) yield(NULL);
        // Check for abort
        if (fde->abort) {
            dprintf(6, "nfs_write: aborting operation\n");
            // Free pinned frame - it's our responsibility
            frame_free(sos_kaddr);
            _nfs_delete_fd((seL4_Word) fde);
            free(pcb);
            return NULL;
        }

        err = _nfs_stat_translate(err);
        if (err) break;

        // Yield and immediately receive the number of bytes written
        recv = (int) yield(NULL);

        // release page, compute next call
        err = sos_page_release(pcb, cur_vaddr);

        // bump counters
        fde->seek += recv;
        sent += recv;
        cur_vaddr += recv;
    }

    sos_syscall_write_reply(pcb, err, sent);
    return NULL;
}

static int _write(sos_pcb *pcb, seL4_Word fs_fd, char* buf, size_t nbyte) {

    int err;
    list args;
    nfs_fd_entry *fde;

    if (nbyte == 0) {
        sos_syscall_write_reply(pcb, SOS_VFS_SUCCESS, 0);
        return SOS_VFS_SUCCESS;
    }

    if (buf == NULL) {
        sos_syscall_write_reply(pcb, SOS_VFS_INVAL, 0);
        return SOS_VFS_INVAL;
    }

    // Grab FDE pointer (address translation - not table lookup)
    err = _nfs_lookup_fd(fs_fd, &fde);
    if (err) {
        sos_syscall_write_reply(pcb, err, 0);
        return err;
    }

    // Check we are allowed to write from this FD
    if (fde->mode != O_WRONLY && fde->mode != O_RDWR) return SOS_VFS_PERM;

    // Pass arguments to the coroutine via a list
    args = list_init();
    err  = list_push_back(args, (SOS_LIST_TYPE) pcb);
    err |= list_push_back(args, (SOS_LIST_TYPE) buf);
    err |= list_push_back(args, (SOS_LIST_TYPE) nbyte);
    err |= list_push_back(args, (SOS_LIST_TYPE) fde);
    if (err) {
        // Kernel is probably out of memory.
        // XXX (We should still call back the process)
        dprintf(3, "nfs_write: Could not allocate task args (%d)\n", err);
        list_destroy(args);
        sos_syscall_write_reply(pcb, SOS_VFS_OOM, 0);
        return SOS_VFS_OOM;
    }

    // Create the coroutine that will do all the actual reading
    fde->task = coroutine(&_write_task);
    // Send its initial arguments
    resume(fde->task, (void *) args);
    list_destroy(args);

    return SOS_VFS_SUCCESS;
}

void *_stat_task(void *args) {
    int err;
    sos_stat_t stat_buf = { 0 };
    sos_pcb *pcb = (sos_pcb *) args;
    fattr_t *fattr;

    dprintf(3, "stat_task is running\n");

    err = (int) yield(NULL);
    err = _nfs_stat_translate(err);
    fattr = (fattr_t *) yield(NULL);

    if (pcb->abort) {
        // all over
        free(pcb);
        return NULL;
    }

    // Translate the attributes, if we got any
    if (err == SOS_VFS_SUCCESS) {
        // Grab filetype - SOS only knows FILE and SPECIAL.
        if (fattr->type == NFREG) {
            stat_buf.st_type = ST_FILE;
        } else {
            // Any filetypes we don't understand are special
            stat_buf.st_type = ST_SPECIAL;
        }

        // Grab permissions - similar to nfs_open
        stat_buf.st_fmode = 0;
        if (MODE_CAN_READ(fattr->mode))  stat_buf.st_fmode |= FM_READ;
        if (MODE_CAN_WRITE(fattr->mode)) stat_buf.st_fmode |= FM_WRITE;
        if (MODE_CAN_EXEC(fattr->mode))  stat_buf.st_fmode |= FM_EXEC;

        // Copy size
        stat_buf.st_size = fattr->size;

        // Copy ctime
        stat_buf.st_ctime = _timeval_sos(fattr->ctime);

        // Copy atime
        stat_buf.st_atime = _timeval_sos(fattr->ctime);
    }

    sos_syscall_stat_reply(pcb, err, stat_buf);
    return NULL;
}

void _stat_cb(uintptr_t token, enum nfs_stat status, fhandle_t *fh,
              fattr_t *fattr) {
    int err;
    nfs_fd_entry *fd = (nfs_fd_entry *) token;

    dprintf(3, "stat callback running\n");
    dprintf(3, "fd is at %p\n", fd);
    dprintf(3, "task is at %p\n", fd->task);
    resume(fd->task, (void *) status);
    resume(fd->task, (void *) fattr);
    assert(!resumable(fd->task));
    // Not an open - don't need to keep the FD around.
    // XXX Need to tidy up the FD interfaces - delete shouldn't require it to be in the table
    free(token);
    return;
}

static int _stat(sos_pcb *pcb, const char *path) {
    int err;
    seL4_Word fs_fd;
    nfs_fd_entry *fd;
    sos_stat_t stat_buf = {0};

    dprintf(3, "nfs_stat: path %.255s\n", path);

    // Allocate a FDE - don't put it in the table yet
    // Call back the process when we're out of memory
    err = _nfs_create_fd(&fs_fd);
    err |= _nfs_lookup_fd(fs_fd, &fd);
    if (err) {
        sos_syscall_stat_reply(pcb, err, stat_buf);
        return err;
    }

    // Set up the coroutine that does the actual work
    fd->task = coroutine(&_stat_task);
    resume(fd->task, (void *) pcb);

    // Set up the nfs_lookup operation. Return the translated rpc_stat.
    err = nfs_lookup(&mnt_point, path, &_stat_cb, (uintptr_t) fd);

    return _rpc_stat_translate(err);
}

void _getdirent_readdir_cb(uintptr_t token, enum nfs_stat status, int num_files,
                           char *file_names[], nfscookie_t nfscookie) {
    int err;
    nfs_fd_entry *fd = (nfs_fd_entry *) token;
    dprintf(3, "readdir callback firing\n");
    list args = list_init();
    err  = list_push_back(args, (SOS_LIST_TYPE) status);
    err |= list_push_back(args, (SOS_LIST_TYPE) num_files);
    err |= list_push_back(args, (SOS_LIST_TYPE) file_names);
    err |= list_push_back(args, (SOS_LIST_TYPE) nfscookie);
    resume(fd->task, (void *) args);
    list_destroy(args);
    return;
}

void *_getdirent_task(void *args) {
    int err;
    list argv = (list) args;

    // Copy everything out of the list so it can be destroyed
    sos_pcb *pcb = (sos_pcb *) list_pop_front(argv);
    nfs_fd_entry *fd = (nfs_fd_entry *) list_pop_front(argv);
    int pos = (int) list_pop_front(argv);
    size_t max = (size_t) list_pop_front(argv);

    // In a loop, set up readdirs. The callback, _getdirent_readdir_cb,
    // will wake us up and (clumsily, for now) send us various parameters.
    nfscookie_t cookie = 0;
    char **file_names;
    int num_files;
    int total_files = 0;
    char *fn;

    while (total_files <= pos) {
        dprintf(3, "setting up another readdir. got %d so far\n", total_files);
        err = nfs_readdir(&mnt_point, cookie, &_getdirent_readdir_cb,
                          (uintptr_t) fd);
        err = _rpc_stat_translate(err);
        if (err) break;

        // Wait for the readdir callback to wake us up
        argv = (list) yield(NULL);

        // See if process has been killed
        if (pcb->abort) {
            free(pcb);
            return NULL;
        }

        // Pull arguments out of argv
        // Grab NFS status
        err = (int) list_pop_front(argv);
        // Grab number of files in current listing
        num_files = (int) list_pop_front(argv);
        // Grab new pointer to filenames
        file_names = (char **) list_pop_front(argv);
        // Grab new NFS cookie
        cookie = (nfscookie_t) list_pop_front(argv);

        // Break and exit if error
        err = _nfs_stat_translate(err);
        if (err) break;

        if (total_files + num_files > pos) {
            // We've got our entry
            err = SOS_VFS_SUCCESS;
            fn = file_names[pos - total_files];
            dprintf(3, "getdirent: found %s\n", fn);
            break;
        } else {
            // Repeat it all
            total_files += num_files;
        }

        // We're done if cookie is 0.
        // If the index is total_files + 1, this is the 'next free'
        // (so we return OK)
        if (cookie == 0 && pos == total_files) {
            fn = NULL;
            err = SOS_VFS_SUCCESS;
            break;
        } else if (cookie == 0) {
            err = SOS_VFS_NOENT;
            break;
        }
    }

    // Call back the waiting process
    sos_syscall_getdirent_reply(pcb, fn,
            ((fn == NULL) ? 0 : 1 + strnlen(fn, SOS_PATH_MAX)),
            err);

    // Destroy FD
    free(fd); // XXX Cleanup interfaces

    return NULL;
}

static int _getdirent(sos_pcb *pcb, int pos, size_t max) {
    int err;
    seL4_Word fs_fd;
    nfs_fd_entry *fd;
    list args;

    dprintf(3, "nfs_getdirent: pos %d\tmaxnbyte %u\n", pos, max);

    // Create FD structure
    err = _nfs_create_fd(&fs_fd);
    if (err) return err;

    // Get pointer to it
    err = _nfs_lookup_fd(fs_fd, &fd);
    if (err) return err;

    // Pass arguments to the coroutine via a list
    args = list_init();
    err  = list_push_back(args, (SOS_LIST_TYPE) pcb);
    err |= list_push_back(args, (SOS_LIST_TYPE) fd);
    err |= list_push_back(args, (SOS_LIST_TYPE) pos);
    err |= list_push_back(args, (SOS_LIST_TYPE) max);
    if (err) {
        // Very bad - we're out of memory, or worse.
        // XXX We should wake up the process here.
        dprintf(3, "nfs_getdirent: Could not allocate task args (%d)\n");
        list_destroy(args);
        return SOS_VFS_OOM;
    }

    // Set up its coroutine
    fd->task = coroutine(&_getdirent_task);

    // Send through its arguments
    resume(fd->task, (void *) args);

    // Clean up
    list_destroy(args);

    // Return to caller
    return SOS_VFS_SUCCESS;
}
